<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Table of contents</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body><script>
$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };

    $("#accordion").accordion({
      collapsible : true,
      active : false,
      icons : icons,
      heightStyle : 'content'
    });

    // Enable navigation links in section headers
    $('#accordion').each(function() {
      this.addEventListener('click', ev => {
        if ($(ev.target).closest('a').length > 0) ev.stopPropagation();
      }, {capture: true});
    });
  } );
</script>


<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>
</div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">Preface</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab1">Welcome</a>

</li>
<li><a href="Preface.html#lab2">Overview</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab3">Program Verification</a>

</li>
<li><a href="Preface.html#lab4">Type Systems</a>

</li>
<li><a href="Preface.html#lab5">Further Reading</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab6">Practicalities</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab7">Recommended Citation Format</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab8">Note for Instructors</a>

</li>
<li><a href="Preface.html#lab9">Thanks</a>

</li>
</ul>
</div>
<h2><a href="Equiv.html">Program Equivalence &nbsp;&nbsp; (<i>Equiv</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab12">Behavioral Equivalence</a>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab13">Definitions</a>

</li>
<li><a href="Equiv.html#lab14">Simple Examples</a>

</li>
</ul>
</div>

</li>
<li><a href="Equiv.html#lab24">Properties of Behavioral Equivalence</a>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab25">Behavioral Equivalence Is an Equivalence</a>

</li>
<li><a href="Equiv.html#lab26">Behavioral Equivalence Is a Congruence</a>

</li>
</ul>
</div>

</li>
<li><a href="Equiv.html#lab30">Program Transformations</a>
<div>
<ul class="doclist">
<li><a href="Equiv.html#lab31">The Constant-Folding Transformation</a>

</li>
<li><a href="Equiv.html#lab32">Soundness of Constant Folding</a>

</li>
</ul>
</div>

</li>
<li><a href="Equiv.html#lab37">Proving Inequivalence</a>

</li>
<li><a href="Equiv.html#lab40">Extended Exercise: Nondeterministic Imp</a>

</li>
<li><a href="Equiv.html#lab48">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Hoare.html">Hoare Logic, Part I &nbsp;&nbsp; (<i>Hoare</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Hoare.html#lab52">Assertions</a>
<div>
<ul class="doclist">
<li><a href="Hoare.html#lab54">Notations for Assertions</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare.html#lab55">Hoare Triples, Informally</a>

</li>
<li><a href="Hoare.html#lab58">Hoare Triples, Formally</a>

</li>
<li><a href="Hoare.html#lab61">Proof Rules</a>
<div>
<ul class="doclist">
<li><a href="Hoare.html#lab62">Assignment</a>

</li>
<li><a href="Hoare.html#lab68">Consequence</a>

</li>
<li><a href="Hoare.html#lab69">Automation</a>

</li>
<li><a href="Hoare.html#lab71">Skip</a>

</li>
<li><a href="Hoare.html#lab72">Sequencing</a>

</li>
<li><a href="Hoare.html#lab76">Conditionals</a>

</li>
<li><a href="Hoare.html#lab83">While Loops</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare.html#lab86">Summary</a>

</li>
<li><a href="Hoare.html#lab87">Additional Exercises</a>
<div>
<ul class="doclist">
<li><a href="Hoare.html#lab88">Havoc</a>

</li>
<li><a href="Hoare.html#lab91">Assert and Assume</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Hoare2.html">Hoare Logic, Part II &nbsp;&nbsp; (<i>Hoare2</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab93">Decorated Programs</a>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab94">Example: Swapping Using Addition and Subtraction</a>

</li>
<li><a href="Hoare2.html#lab95">Example: Simple Conditionals</a>

</li>
<li><a href="Hoare2.html#lab97">Example: Reduce to Zero</a>

</li>
<li><a href="Hoare2.html#lab98">Example: Division</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare2.html#lab99">Finding Loop Invariants</a>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab100">Example: Slow Subtraction</a>

</li>
<li><a href="Hoare2.html#lab101">Exercise: Slow Assignment</a>

</li>
<li><a href="Hoare2.html#lab103">Exercise: Slow Addition</a>

</li>
<li><a href="Hoare2.html#lab105">Example: Parity</a>

</li>
<li><a href="Hoare2.html#lab107">Example: Finding Square Roots</a>

</li>
<li><a href="Hoare2.html#lab108">Example: Squaring</a>

</li>
<li><a href="Hoare2.html#lab109">Exercise: Factorial</a>

</li>
<li><a href="Hoare2.html#lab111">Exercise: Min</a>

</li>
<li><a href="Hoare2.html#lab114">Exercise: Power Series</a>

</li>
</ul>
</div>

</li>
<li><a href="Hoare2.html#lab116">Weakest Preconditions (Optional)</a>

</li>
<li><a href="Hoare2.html#lab121">Formal Decorated Programs (Advanced)</a>
<div>
<ul class="doclist">
<li><a href="Hoare2.html#lab122">Syntax</a>

</li>
<li><a href="Hoare2.html#lab123">Extracting Verification Conditions</a>

</li>
<li><a href="Hoare2.html#lab124">Automation</a>

</li>
<li><a href="Hoare2.html#lab132">Further Exercises</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="HoareAsLogic.html">Hoare Logic as a Logic &nbsp;&nbsp; (<i>HoareAsLogic</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="HoareAsLogic.html#lab138">Hoare Logic and Model Theory</a>

</li>
<li><a href="HoareAsLogic.html#lab139">Hoare Logic and Proof Theory</a>

</li>
<li><a href="HoareAsLogic.html#lab140">Derivability</a>

</li>
<li><a href="HoareAsLogic.html#lab143">Soundness and Completeness</a>

</li>
<li><a href="HoareAsLogic.html#lab148">Postscript: Decidability</a>

</li>
</ul>
</div>
<h2><a href="Smallstep.html">Small-step Operational Semantics &nbsp;&nbsp; (<i>Smallstep</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Smallstep.html#lab149">A Toy Language</a>

</li>
<li><a href="Smallstep.html#lab151">Relations</a>
<div>
<ul class="doclist">
<li><a href="Smallstep.html#lab152">Values</a>

</li>
<li><a href="Smallstep.html#lab154">Strong Progress and Normal Forms</a>

</li>
</ul>
</div>

</li>
<li><a href="Smallstep.html#lab164">Multi-Step Reduction</a>
<div>
<ul class="doclist">
<li><a href="Smallstep.html#lab165">Examples</a>

</li>
<li><a href="Smallstep.html#lab169">Normal Forms Again</a>

</li>
<li><a href="Smallstep.html#lab172">Equivalence of Big-Step and Small-Step</a>

</li>
<li><a href="Smallstep.html#lab177">Additional Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Smallstep.html#lab180">Small-Step Imp</a>

</li>
<li><a href="Smallstep.html#lab181">Concurrent Imp</a>

</li>
<li><a href="Smallstep.html#lab184">A Small-Step Stack Machine</a>

</li>
<li><a href="Smallstep.html#lab186">Aside: A <span class="inlinecode"><span class="id" title="var">normalize</span></span> Tactic</a>

</li>
</ul>
</div>
<h2><a href="Types.html">Type Systems &nbsp;&nbsp; (<i>Types</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Types.html#lab189">Typed Arithmetic Expressions</a>
<div>
<ul class="doclist">
<li><a href="Types.html#lab190">Syntax</a>

</li>
<li><a href="Types.html#lab191">Operational Semantics</a>

</li>
<li><a href="Types.html#lab192">Normal Forms and Values</a>

</li>
<li><a href="Types.html#lab196">Typing</a>

</li>
<li><a href="Types.html#lab199">Progress</a>

</li>
<li><a href="Types.html#lab202">Type Preservation</a>

</li>
<li><a href="Types.html#lab206">Type Soundness</a>

</li>
<li><a href="Types.html#lab207">Additional Exercises</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Stlc.html">The Simply Typed Lambda-Calculus &nbsp;&nbsp; (<i>Stlc</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab218">Overview</a>

</li>
<li><a href="Stlc.html#lab219">Syntax</a>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab220">Types</a>

</li>
<li><a href="Stlc.html#lab221">Terms</a>

</li>
</ul>
</div>

</li>
<li><a href="Stlc.html#lab222">Operational Semantics</a>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab223">Values</a>

</li>
<li><a href="Stlc.html#lab224">Substitution</a>

</li>
<li><a href="Stlc.html#lab226">Reduction</a>

</li>
<li><a href="Stlc.html#lab227">Examples</a>

</li>
</ul>
</div>

</li>
<li><a href="Stlc.html#lab229">Typing</a>
<div>
<ul class="doclist">
<li><a href="Stlc.html#lab230">Contexts</a>

</li>
<li><a href="Stlc.html#lab231">Typing Relation</a>

</li>
<li><a href="Stlc.html#lab232">Examples</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="StlcProp.html">Properties of STLC &nbsp;&nbsp; (<i>StlcProp</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="StlcProp.html#lab236">Canonical Forms</a>

</li>
<li><a href="StlcProp.html#lab237">Progress</a>

</li>
<li><a href="StlcProp.html#lab239">Preservation</a>
<div>
<ul class="doclist">
<li><a href="StlcProp.html#lab240">The Weakening Lemma</a>

</li>
<li><a href="StlcProp.html#lab241">A Substitution Lemma</a>

</li>
<li><a href="StlcProp.html#lab243">Main Theorem</a>

</li>
</ul>
</div>

</li>
<li><a href="StlcProp.html#lab245">Type Soundness</a>

</li>
<li><a href="StlcProp.html#lab247">Uniqueness of Types</a>

</li>
<li><a href="StlcProp.html#lab249">Context Invariance (Optional)</a>

</li>
<li><a href="StlcProp.html#lab254">Additional Exercises</a>
<div>
<ul class="doclist">
<li><a href="StlcProp.html#lab263">Exercise: STLC with Arithmetic</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="MoreStlc.html">More on the Simply Typed Lambda-Calculus &nbsp;&nbsp; (<i>MoreStlc</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="MoreStlc.html#lab265">Simple Extensions to STLC</a>
<div>
<ul class="doclist">
<li><a href="MoreStlc.html#lab266">Numbers</a>

</li>
<li><a href="MoreStlc.html#lab267">Let Bindings</a>

</li>
<li><a href="MoreStlc.html#lab268">Pairs</a>

</li>
<li><a href="MoreStlc.html#lab269">Unit</a>

</li>
<li><a href="MoreStlc.html#lab270">Sums</a>

</li>
<li><a href="MoreStlc.html#lab271">Lists</a>

</li>
<li><a href="MoreStlc.html#lab272">General Recursion</a>

</li>
<li><a href="MoreStlc.html#lab275">Records</a>

</li>
</ul>
</div>

</li>
<li><a href="MoreStlc.html#lab278">Exercise: Formalizing the Extensions</a>
<div>
<ul class="doclist">
<li><a href="MoreStlc.html#lab284">Examples</a>

</li>
<li><a href="MoreStlc.html#lab293">Properties of Typing</a>

</li>
<li><a href="MoreStlc.html#lab296">Weakening</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Sub.html">Subtyping &nbsp;&nbsp; (<i>Sub</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab301">Concepts</a>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab302">A Motivating Example</a>

</li>
<li><a href="Sub.html#lab303">Subtyping and Object-Oriented Languages</a>

</li>
<li><a href="Sub.html#lab304">The Subsumption Rule</a>

</li>
<li><a href="Sub.html#lab305">The Subtype Relation</a>

</li>
<li><a href="Sub.html#lab313">Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Sub.html#lab327">Formal Definitions</a>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab328">Core Definitions</a>

</li>
<li><a href="Sub.html#lab332">Subtyping</a>

</li>
<li><a href="Sub.html#lab336">Typing</a>

</li>
</ul>
</div>

</li>
<li><a href="Sub.html#lab340">Properties</a>
<div>
<ul class="doclist">
<li><a href="Sub.html#lab341">Inversion Lemmas for Subtyping</a>

</li>
<li><a href="Sub.html#lab344">Canonical Forms</a>

</li>
<li><a href="Sub.html#lab346">Progress</a>

</li>
<li><a href="Sub.html#lab347">Inversion Lemmas for Typing</a>

</li>
<li><a href="Sub.html#lab350">Weakening</a>

</li>
<li><a href="Sub.html#lab351">Substitution</a>

</li>
<li><a href="Sub.html#lab352">Preservation</a>

</li>
<li><a href="Sub.html#lab353">Records, via Products and Top</a>

</li>
<li><a href="Sub.html#lab354">Exercises</a>

</li>
</ul>
</div>

</li>
<li><a href="Sub.html#lab356">Exercise: Adding Products</a>

</li>
</ul>
</div>
<h2><a href="Typechecking.html">A Typechecker for STLC &nbsp;&nbsp; (<i>Typechecking</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Typechecking.html#lab358">Comparing Types</a>

</li>
<li><a href="Typechecking.html#lab359">The Typechecker</a>

</li>
<li><a href="Typechecking.html#lab360">Digression: Improving the Notation</a>

</li>
<li><a href="Typechecking.html#lab361">Properties</a>

</li>
<li><a href="Typechecking.html#lab362">Exercises</a>

</li>
</ul>
</div>
<h2><a href="Records.html">Adding Records to STLC &nbsp;&nbsp; (<i>Records</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Records.html#lab366">Adding Records</a>

</li>
<li><a href="Records.html#lab367">Formalizing Records</a>
<div>
<ul class="doclist">
<li><a href="Records.html#lab373">Examples</a>

</li>
<li><a href="Records.html#lab375">Properties of Typing</a>

</li>
<li><a href="Records.html#lab379">Weakening</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="References.html">Typing Mutable References &nbsp;&nbsp; (<i>References</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="References.html#lab381">Definitions</a>

</li>
<li><a href="References.html#lab382">Syntax</a>

</li>
<li><a href="References.html#lab387">Pragmatics</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab388">Side Effects and Sequencing</a>

</li>
<li><a href="References.html#lab389">References and Aliasing</a>

</li>
<li><a href="References.html#lab390">Shared State</a>

</li>
<li><a href="References.html#lab391">Objects</a>

</li>
<li><a href="References.html#lab393">References to Compound Types</a>

</li>
<li><a href="References.html#lab395">Null References</a>

</li>
<li><a href="References.html#lab396">Garbage Collection</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab398">Operational Semantics</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab399">Locations</a>

</li>
<li><a href="References.html#lab400">Stores</a>

</li>
<li><a href="References.html#lab401">Reduction</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab402">Typing</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab403">Store typings</a>

</li>
<li><a href="References.html#lab405">The Typing Relation</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab406">Properties</a>
<div>
<ul class="doclist">
<li><a href="References.html#lab407">Well-Typed Stores</a>

</li>
<li><a href="References.html#lab409">Extending Store Typings</a>

</li>
<li><a href="References.html#lab410">Preservation, Finally</a>

</li>
<li><a href="References.html#lab411">Substitution Lemma</a>

</li>
<li><a href="References.html#lab412">Assignment Preserves Store Typing</a>

</li>
<li><a href="References.html#lab413">Weakening for Stores</a>

</li>
<li><a href="References.html#lab414">Preservation!</a>

</li>
<li><a href="References.html#lab416">Progress</a>

</li>
</ul>
</div>

</li>
<li><a href="References.html#lab417">References and Nontermination</a>

</li>
<li><a href="References.html#lab419">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="RecordSub.html">Subtyping with Records &nbsp;&nbsp; (<i>RecordSub</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="RecordSub.html#lab421">Core Definitions</a>

</li>
<li><a href="RecordSub.html#lab426">Subtyping</a>
<div>
<ul class="doclist">
<li><a href="RecordSub.html#lab427">Definition</a>

</li>
<li><a href="RecordSub.html#lab428">Examples</a>

</li>
<li><a href="RecordSub.html#lab433">Properties of Subtyping</a>

</li>
</ul>
</div>

</li>
<li><a href="RecordSub.html#lab439">Typing</a>
<div>
<ul class="doclist">
<li><a href="RecordSub.html#lab440">Typing Examples</a>

</li>
<li><a href="RecordSub.html#lab444">Properties of Typing</a>

</li>
<li><a href="RecordSub.html#lab450">Weakening</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Norm.html">Normalization of STLC &nbsp;&nbsp; (<i>Norm</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Norm.html#lab454">Language</a>
<div>
<ul class="doclist">
<li><a href="Norm.html#lab459">Weakening</a>

</li>
</ul>
</div>

</li>
<li><a href="Norm.html#lab464">Normalization</a>
<div>
<ul class="doclist">
<li><a href="Norm.html#lab465">Membership in <span class="inlinecode"><span class="id" title="var">R_T</span></span> Is Invariant Under Reduction</a>

</li>
<li><a href="Norm.html#lab466">Closed Instances of Terms of Type <span class="inlinecode"><span class="id" title="var">t</span></span> Belong to <span class="inlinecode"><span class="id" title="var">R_T</span></span></a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="PE.html">Partial Evaluation &nbsp;&nbsp; (<i>PE</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="PE.html#lab475">Generalizing Constant Folding</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab476">Partial States</a>

</li>
<li><a href="PE.html#lab477">Arithmetic Expressions</a>

</li>
<li><a href="PE.html#lab478">Boolean Expressions</a>

</li>
</ul>
</div>

</li>
<li><a href="PE.html#lab479">Partial Evaluation of Commands, Without Loops</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab480">Assignment</a>

</li>
<li><a href="PE.html#lab481">Conditional</a>

</li>
<li><a href="PE.html#lab482">The Partial Evaluation Relation</a>

</li>
<li><a href="PE.html#lab483">Examples</a>

</li>
<li><a href="PE.html#lab484">Correctness of Partial Evaluation</a>

</li>
</ul>
</div>

</li>
<li><a href="PE.html#lab485">Partial Evaluation of Loops</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab486">Examples</a>

</li>
<li><a href="PE.html#lab487">Correctness</a>

</li>
</ul>
</div>

</li>
<li><a href="PE.html#lab488">Partial Evaluation of Flowchart Programs</a>
<div>
<ul class="doclist">
<li><a href="PE.html#lab489">Basic blocks</a>

</li>
<li><a href="PE.html#lab490">Flowchart programs</a>

</li>
<li><a href="PE.html#lab491">Partial Evaluation of Basic Blocks and Flowchart Programs</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Postscript.html">Postscript</a></h2>
<div>
<ul class="doclist">
<li><a href="Postscript.html#lab492">Looking Back</a>

</li>
<li><a href="Postscript.html#lab493">Looking Around</a>

</li>
<li><a href="Postscript.html#lab502">Looking Forward</a>

</li>
</ul>
</div>
<h2><a href="Bib.html">Bibliography &nbsp;&nbsp; (<i>Bib</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Bib.html#lab503">Resources cited in this volume</a>

</li>
</ul>
</div>
<h2><a href="LibTactics.html">A Collection of Handy General-Purpose Tactics &nbsp;&nbsp; (<i>LibTactics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab504">Fixing Stdlib</a>

</li>
<li><a href="LibTactics.html#lab505">Tools for Programming with Ltac</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab506">Identity Continuation</a>

</li>
<li><a href="LibTactics.html#lab507">Untyped Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab508">Optional Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab509">Wildcard Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab510">Position Markers</a>

</li>
<li><a href="LibTactics.html#lab511">List of Arguments for Tactics</a>

</li>
<li><a href="LibTactics.html#lab512">Databases of Lemmas</a>

</li>
<li><a href="LibTactics.html#lab513">On-the-Fly Removal of Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab514">Numbers as Arguments</a>

</li>
<li><a href="LibTactics.html#lab515">Testing Tactics</a>

</li>
<li><a href="LibTactics.html#lab516">Testing evars and non-evars</a>

</li>
<li><a href="LibTactics.html#lab517">Check No Evar in Goal</a>

</li>
<li><a href="LibTactics.html#lab518">Helper Function for Introducing Evars</a>

</li>
<li><a href="LibTactics.html#lab519">Tagging of Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab520">More Tagging of Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab521">Deconstructing Terms</a>

</li>
<li><a href="LibTactics.html#lab522">Action at Occurence and Action Not at Occurence</a>

</li>
<li><a href="LibTactics.html#lab523">An Alias for <span class="inlinecode"><span class="id" title="var">eq</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab524">Common Tactics for Simplifying Goals Like <span class="inlinecode"><span class="id" title="tactic">intuition</span></span></a>

</li>
<li><a href="LibTactics.html#lab525">Backward and Forward Chaining</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab526">Application</a>

</li>
<li><a href="LibTactics.html#lab527">Assertions</a>

</li>
<li><a href="LibTactics.html#lab528">Instantiation and Forward-Chaining</a>

</li>
<li><a href="LibTactics.html#lab529">Experimental Tactics for Application</a>

</li>
<li><a href="LibTactics.html#lab530">Adding Assumptions</a>

</li>
<li><a href="LibTactics.html#lab531">Application of Tautologies</a>

</li>
<li><a href="LibTactics.html#lab532">Application Modulo Equalities</a>

</li>
<li><a href="LibTactics.html#lab533">Absurd Goals</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab534">Introduction and Generalization</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab535">Introduction</a>

</li>
<li><a href="LibTactics.html#lab536">Introduction using <span class="inlinecode">⇒</span> and <span class="inlinecode">=&gt;&gt;</span></a>

</li>
<li><a href="LibTactics.html#lab537">Generalization</a>

</li>
<li><a href="LibTactics.html#lab538">Naming</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab539">Rewriting</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab540">Replace</a>

</li>
<li><a href="LibTactics.html#lab541">Change</a>

</li>
<li><a href="LibTactics.html#lab542">Renaming</a>

</li>
<li><a href="LibTactics.html#lab543">Unfolding</a>

</li>
<li><a href="LibTactics.html#lab544">Simplification</a>

</li>
<li><a href="LibTactics.html#lab545">Reduction</a>

</li>
<li><a href="LibTactics.html#lab546">Substitution</a>

</li>
<li><a href="LibTactics.html#lab547">Tactics to Work with Proof Irrelevance</a>

</li>
<li><a href="LibTactics.html#lab548">Proving Equalities</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab549">Inversion</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab550">Basic Inversion</a>

</li>
<li><a href="LibTactics.html#lab551">Inversion with Substitution</a>

</li>
<li><a href="LibTactics.html#lab552">Injection with Substitution</a>

</li>
<li><a href="LibTactics.html#lab553">Inversion and Injection with Substitution --rough implementation</a>

</li>
<li><a href="LibTactics.html#lab554">Case Analysis</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab555">Induction</a>

</li>
<li><a href="LibTactics.html#lab556">Coinduction</a>

</li>
<li><a href="LibTactics.html#lab557">Decidable Equality</a>

</li>
<li><a href="LibTactics.html#lab558">Equivalence</a>

</li>
<li><a href="LibTactics.html#lab559">N-ary Conjunctions and Disjunctions</a>

</li>
<li><a href="LibTactics.html#lab560">Tactics to Prove Typeclass Instances</a>

</li>
<li><a href="LibTactics.html#lab561">Tactics to Invoke Automation</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab562">Definitions for Parsing Compatibility</a>

</li>
<li><a href="LibTactics.html#lab563"><span class="inlinecode"><span class="id" title="var">hint</span></span> to Add Hints Local to a Lemma</a>

</li>
<li><a href="LibTactics.html#lab564"><span class="inlinecode"><span class="id" title="var">jauto</span></span>, a New Automation Tactic</a>

</li>
<li><a href="LibTactics.html#lab565">Definitions of Automation Tactics</a>

</li>
<li><a href="LibTactics.html#lab566">Parsing for Light Automation</a>

</li>
<li><a href="LibTactics.html#lab567">Parsing for Strong Automation</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab568">Tactics to Sort Out the Proof Context</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab569">Hiding Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab570">Sorting Hypotheses</a>

</li>
<li><a href="LibTactics.html#lab571">Clearing Hypotheses</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab572">Tactics for Development Purposes</a>
<div>
<ul class="doclist">
<li><a href="LibTactics.html#lab573">Skipping Subgoals</a>

</li>
</ul>
</div>

</li>
<li><a href="LibTactics.html#lab574">Compatibility with standard library</a>

</li>
</ul>
</div>
<h2><a href="UseTactics.html">Tactic Library for Coq: A Gentle Introduction &nbsp;&nbsp; (<i>UseTactics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab575">Tactics for Naming and Performing Inversion</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab576">The Tactic <span class="inlinecode"><span class="id" title="var">introv</span></span></a>

</li>
<li><a href="UseTactics.html#lab577">The Tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab578">Tactics for N-ary Connectives</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab579">The Tactic <span class="inlinecode"><span class="id" title="var">splits</span></span></a>

</li>
<li><a href="UseTactics.html#lab580">The Tactic <span class="inlinecode"><span class="id" title="var">branch</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab581">Tactics for Working with Equality</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab582">The Tactics <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> and <span class="inlinecode"><span class="id" title="var">cuts_rewrite</span></span></a>

</li>
<li><a href="UseTactics.html#lab583">The Tactic <span class="inlinecode"><span class="id" title="var">substs</span></span></a>

</li>
<li><a href="UseTactics.html#lab584">The Tactic <span class="inlinecode"><span class="id" title="var">fequals</span></span></a>

</li>
<li><a href="UseTactics.html#lab585">The Tactic <span class="inlinecode"><span class="id" title="var">applys_eq</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab586">Some Convenient Shorthands</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab587">The Tactic <span class="inlinecode"><span class="id" title="var">unfolds</span></span></a>

</li>
<li><a href="UseTactics.html#lab588">The Tactics <span class="inlinecode"><span class="id" title="var">false</span></span> and <span class="inlinecode"><span class="id" title="var">tryfalse</span></span></a>

</li>
<li><a href="UseTactics.html#lab589">The Tactic <span class="inlinecode"><span class="id" title="var">gen</span></span></a>

</li>
<li><a href="UseTactics.html#lab590">The Tactics <span class="inlinecode"><span class="id" title="var">admits</span></span>, <span class="inlinecode"><span class="id" title="var">admit_rewrite</span></span> and <span class="inlinecode"><span class="id" title="var">admit_goal</span></span></a>

</li>
<li><a href="UseTactics.html#lab591">The Tactic <span class="inlinecode"><span class="id" title="var">sort</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab592">Tactics for Advanced Lemma Instantiation</a>
<div>
<ul class="doclist">
<li><a href="UseTactics.html#lab593">Working of <span class="inlinecode"><span class="id" title="var">lets</span></span></a>

</li>
<li><a href="UseTactics.html#lab594">Working of <span class="inlinecode"><span class="id" title="var">applys</span></span>, <span class="inlinecode"><span class="id" title="var">forwards</span></span> and <span class="inlinecode"><span class="id" title="var">specializes</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="UseTactics.html#lab595">Summary</a>

</li>
</ul>
</div>
<h2><a href="UseAuto.html">Theory and Practice of Automation in Coq Proofs &nbsp;&nbsp; (<i>UseAuto</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab596">Basic Features of Proof Search</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab597">Strength of Proof Search</a>

</li>
<li><a href="UseAuto.html#lab598">Basics</a>

</li>
<li><a href="UseAuto.html#lab599">Conjunctions</a>

</li>
<li><a href="UseAuto.html#lab600">Disjunctions</a>

</li>
<li><a href="UseAuto.html#lab601">Existentials</a>

</li>
<li><a href="UseAuto.html#lab602">Negation</a>

</li>
<li><a href="UseAuto.html#lab603">Equalities</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab604">How Proof Search Works</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab605">Search Depth</a>

</li>
<li><a href="UseAuto.html#lab606">Backtracking</a>

</li>
<li><a href="UseAuto.html#lab607">Adding Hints</a>

</li>
<li><a href="UseAuto.html#lab608">Integration of Automation in Tactics</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab609">Example Proofs using Automation</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab610">Determinism</a>

</li>
<li><a href="UseAuto.html#lab611">Preservation for STLC</a>

</li>
<li><a href="UseAuto.html#lab612">Progress for STLC</a>

</li>
<li><a href="UseAuto.html#lab613">BigStep and SmallStep</a>

</li>
<li><a href="UseAuto.html#lab614">Preservation for STLCRef</a>

</li>
<li><a href="UseAuto.html#lab615">Progress for STLCRef</a>

</li>
<li><a href="UseAuto.html#lab616">Subtyping</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab617">Advanced Topics in Proof Search</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab618">Stating Lemmas in the Right Way</a>

</li>
<li><a href="UseAuto.html#lab619">Unfolding of Definitions During Proof-Search</a>

</li>
<li><a href="UseAuto.html#lab620">Automation for Proving Absurd Goals</a>

</li>
<li><a href="UseAuto.html#lab621">Automation for Transitivity Lemmas</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab622">Decision Procedures</a>
<div>
<ul class="doclist">
<li><a href="UseAuto.html#lab623">Lia</a>

</li>
<li><a href="UseAuto.html#lab624">Ring</a>

</li>
<li><a href="UseAuto.html#lab625">Congruence</a>

</li>
</ul>
</div>

</li>
<li><a href="UseAuto.html#lab626">Summary</a>

</li>
</ul>
</div>
</div>

</div>

</div>

</div>
</body>
</html>